p:FinProbSpace, n:, X, Y:RandomVariable(p;n).
rv-disjoint(p;n;X;Y)
 (0 < n)
 ((x, y:Outcome. rv-shift(x;X) = rv-shift(y;X)  RandomVariable(p;n - 1))
  (x, y:Outcome. rv-shift(x;Y) = rv-shift(y;Y)  RandomVariable(p;n - 1))) 

latex

Definitions	#$n, FinProbSpace, rv-disjoint(p;n;X;Y), P  Q, {T}, , rv-shift(x;X), <a, b>, if b then t else f fi , left + right, Unit, P  Q, (i = j), , b, b, x:A  B(x), x.A(x), f(a), cons-seq(x;s), suptype(S; T), , T, Type, s = t, , RandomVariable(p;n), Void, a < b, n+m, -n, n - m, True, {i..j}, , {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, S  T, x:AB(x), Outcome, x:A. B(x), t  T
Lemmas	p-outcome wf, le wf, int seg wf, true wf, squash wf, cons-seq wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, rv-shift wf, random-variable wf, finite-prob-space wf, nat wf, rv-disjoint wf